; <!-- 3 -->
; <lemma>
;  <title></title>
;  <origin>BepiColombo_Models_V3.3 | csw_C0 | thm10/THM</origin>
;  <theories>
;    <theory name="basic_relation"/>
;    <theory name="integer"/>
;  </theories>
;  <typenv>
;    <variable name="TC" type="Int<->Int"/>
;    <variable name="TM" type="Int<->Int"/>
;  </typenv>
;  <hypothesis needed="true">TC = {3 |-> 5,3 |-> 6,3 |-> 129,
;                                  6 |-> 2,6 |-> 5,6 |-> 9,
;                                  9 |-> 129,
;                                  17 |-> 1, 17 |-> 128, 
;                                  21 |-> 1,21 |-> 2,21 |-> 128,21 |-> 129,
;                                  200 |-> 1,200 |-> 2,200 |-> 3,200 |-> 4,200 |-> 5,200 |-> 6,200 |-> 7,
;                                  201 |-> 1,201 |-> 2,201 |-> 3,201 |-> 4,201 |-> 5,201 |-> 6,201 |-> 7,201 |-> 8,201 |-> 9,201 |-> 10,
;                                  202 |-> 1,202 |-> 2,202 |-> 3,202 |-> 4,
;                                  203 |-> 1,203 |-> 2,203 |-> 3,203 |-> 4,203 |-> 5,203 |-> 6,203 |-> 7,203 |-> 8,203 |-> 9}</hypothesis>
;  <hypothesis needed="true">TM = {1 |-> 1,1 |-> 2,1 |-> 7,1 |-> 8,
;                                  3 |-> 25,
;                                  5 |-> 1,5 |-> 2,5 |-> 3,5 |-> 4,
;                                  6 |-> 6,6 |-> 10,17 |-> 2,21 |-> 3}</hypothesis>
;  <goal>TC /\ TM = {}</goal>
; </lemma>

(benchmark bepi_colombo_thm10
  :logic UNKNOWN
  :extrapreds ((TC Int Int) 
		(TM Int Int))
  :extramacros ((pair (lambda (?e1 't) (?e2 't) .
			(lambda (?f1 't) (?f2 't) .
			  (and (= ?f1 ?e1) (= ?f2 ?e2)))))
		 (enum1 
		   (lambda (?s1 Int) (?s2 Int) . 
		     (or
		       (= (pair ?s1 ?s2) (pair 3 5))
		       (= (pair ?s1 ?s2) (pair 3 6))
		       (= (pair ?s1 ?s2) (pair 3 129))
		       (= (pair ?s1 ?s2) (pair 6 2))
		       (= (pair ?s1 ?s2) (pair 6 5))
		       (= (pair ?s1 ?s2) (pair 6 9))
		       (= (pair ?s1 ?s2) (pair 9 129))
		       (= (pair ?s1 ?s2) (pair 17 1))
		       (= (pair ?s1 ?s2) (pair 17 128))
		       (= (pair ?s1 ?s2) (pair 21 1))
		       (= (pair ?s1 ?s2) (pair 21 2))
		       (= (pair ?s1 ?s2) (pair 21 128))
		       (= (pair ?s1 ?s2) (pair 21 129))
		       (= (pair ?s1 ?s2) (pair 200 1))
		       (= (pair ?s1 ?s2) (pair 200 2))
		       (= (pair ?s1 ?s2) (pair 200 3))
		       (= (pair ?s1 ?s2) (pair 200 4))
		       (= (pair ?s1 ?s2) (pair 200 5))
		       (= (pair ?s1 ?s2) (pair 200 6))
		       (= (pair ?s1 ?s2) (pair 200 7))
		       (= (pair ?s1 ?s2) (pair 201 1))
		       (= (pair ?s1 ?s2) (pair 201 2))
		       (= (pair ?s1 ?s2) (pair 201 3))
		       (= (pair ?s1 ?s2) (pair 201 4))
		       (= (pair ?s1 ?s2) (pair 201 5))
		       (= (pair ?s1 ?s2) (pair 201 6))
		       (= (pair ?s1 ?s2) (pair 201 7))
		       (= (pair ?s1 ?s2) (pair 201 8))
		       (= (pair ?s1 ?s2) (pair 201 9))
		       (= (pair ?s1 ?s2) (pair 201 10))
		       (= (pair ?s1 ?s2) (pair 202 1))
		       (= (pair ?s1 ?s2) (pair 202 2))
		       (= (pair ?s1 ?s2) (pair 202 3))
		       (= (pair ?s1 ?s2) (pair 202 4))
		       (= (pair ?s1 ?s2) (pair 203 1))
		       (= (pair ?s1 ?s2) (pair 203 2))
		       (= (pair ?s1 ?s2) (pair 203 3))
		       (= (pair ?s1 ?s2) (pair 203 4))
		       (= (pair ?s1 ?s2) (pair 203 5))
		       (= (pair ?s1 ?s2) (pair 203 6))
		       (= (pair ?s1 ?s2) (pair 203 7))
		       (= (pair ?s1 ?s2) (pair 203 8))
		       (= (pair ?s1 ?s2) (pair 203 9)))))
		 (enum2 
		   (lambda (?s1 Int) (?s2 Int) . 
		     (or 
		       (= (pair ?s1 ?s2) (pair 1 1))
		       (= (pair ?s1 ?s2) (pair 1 2))
		       (= (pair ?s1 ?s2) (pair 1 7))
		       (= (pair ?s1 ?s2) (pair 1 8))
		       (= (pair ?s1 ?s2) (pair 3 25))
		       (= (pair ?s1 ?s2) (pair 5 1))
		       (= (pair ?s1 ?s2) (pair 5 2))
		       (= (pair ?s1 ?s2) (pair 5 3))
		       (= (pair ?s1 ?s2) (pair 5 4))
		       (= (pair ?s1 ?s2) (pair 6 6))
		       (= (pair ?s1 ?s2) (pair 6 10))
		       (= (pair ?s1 ?s2) (pair 17 2))
		       (= (pair ?s1 ?s2) (pair 21 3))
		       )))
		 (emptyset2 (lambda (?x 't1) (?y 't2). false))
		 (intersection2 (lambda (?p ('t1 't2 boolean)) (?q ('t1 't2 boolean)) .
				  (lambda (?x 't1) (?y 't2) . (and (?p ?x ?y) (?q ?x ?y)))))
		 )
  :assumption (= TC enum1)
  :assumption (= TM enum2)
  :formula
  (not
      (= emptyset2 (intersection2 TC TM))
    )
)
    